import java.util.HashMap;
import java.util.ArrayList;;


public class State {

	//<Train,Seg>  
	public HashMap trains;
	//@ invariant trains.keySet().elementType == \type(Train);
	//@ invariant trains.entrySet().elementType == \type(Seg);
	
	//so existe um train em cada track, ou seja, nao existem valores do hashmap trains repetidos
	//@ invariant trains.keySet().size() == trains.entrySet().size();	
	
	//nas tracks sobrepostas, de uma track onde se encontra um Train, nao podem existir Trains, ou seja, 
	//as tracks sobrepostas de uma track que tem Train nao pode estar nos valores do hashmap trains.  
	/* invariant (\forall int i;i>=0 && i< trains.size(); trains.values().toArray()[i] instanceof Track &&
	  (\forall int j;j>=0 && j < ((Track) trains.values().toArray()[i]).overlaps.size();
	   !trains.containsValue(((Track)trains.values().toArray()[i]).overlaps.get(j))   ) ); */

	public ArrayList reds;
	//@ invariant reds.elementType == \type(Semaphore);
	public ArrayList ons;
	//@ invariant ons.elementType == \type(Point);
	
	public State() {
		
		trains = new HashMap();
		//@ set trains.keySet().elementType = \type(Train);
		//@ set trains.entrySet().elementType = \type(Seg);
		reds = new ArrayList();
		//@ set reds.elementType = \type(Semaphore);
		ons = new ArrayList();
		//@ set ons.elementType = \type(Point);
		
	}
	
	//@ requires reds != null && ons !=null && trains!=null && n_trains!=null && n_reds !=null && n_ons!=null;
	//@ requires n_ons.elementType == \type(Point) && n_reds.elementType == \type(Semaphore);
	//@ requires n_trains.keySet().size() == n_trains.entrySet().size();
	//@ requires n_trains.keySet().elementType == \type(Train) && n_trains.entrySet().elementType == \type(Seg);
	//@ requires n_ons.elementType == \type(Point);
	public State( HashMap n_trains, ArrayList n_reds, ArrayList n_ons) {
		this.trains = n_trains;
		//@ set trains.keySet().elementType = \type(Train);
		//@ set trains.entrySet().elementType = \type(Seg);
		this.reds = n_reds;
		//@ set reds.elementType = \type(Semaphore);
		this.ons = n_ons;
		//@ set ons.elementType = \type(Point);
	}
	
	
	//@ requires trains.keySet().contains(t) && trains != null;
	private void moveTrain(Train t) throws CantMoveException{
		
		Object track = trains.get(t);
		if (track instanceof Seg) {
			Seg seg = (Seg) track;
			trains.remove(t);
			if (seg.next != null) trains.put(t,seg.next);
		}else{
			throw new CantMoveException("");
		}
	}
	
	//@ requires !trains.keySet().contains(t) && s != null && trains != null;
	private void addTrain(Train t,Seg s)  throws CantAddTrainException{
		if( !trains.keySet().contains(t) && s != null && trains != null ) trains.put(t,s);
		else throw new CantAddTrainException();
	}
	
	public HashMap getTrains() {
		return trains;
	}

	/* requires (\forall int i;i>=0 && i< n_trains.size(); 
	  n_trains != null && 
	  (\forall int j;j>=0 && j < ((Track) n_trains.values().toArray()[i]).overlaps.size();
	   !n_trains.containsValue(((Track)n_trains.values().toArray()[i]).overlaps.get(j))   ) ); 
	public void setTrains(HashMap n_trains) {
		this.trains = n_trains;
	}*/

	public ArrayList getReds() {
		return reds;
	}

	//@ requires this.reds!= null && n_reds != null && n_reds.elementType == \type(Semaphore);
	public void setReds(ArrayList n_reds) {
		this.reds = n_reds;
		//@ set this.reds.elementType = \type(Semaphore);
	}

	public ArrayList  getOns() {
		return ons; 
	}

	//@ requires ons!=null && n_ons.elementType == \type(Point) && n_ons!=null;
	private void setOns(ArrayList n_ons) {
		this.ons = n_ons; 
		//@ set this.ons.elementType = \type(Point);
	}

	//@ requires reds != null;
	private void setRed(Seg t){
		this.reds.add(t.sema);
	}
	
	//@ requires reds != null && t != null && t.n < t.nexts.length;
	private void setGreen( Seg t) throws CantSetGreenException {
		if(t instanceof Track){
			Track tr = (Track) t;
			ArrayList over = tr.getOverlaps();
			if(over!=null){
				for(int i=0;i<over.size();i++){
					Track overlap = (Track) over.get(i);
					if(!this.reds.contains( overlap.sema )){
						throw new CantSetGreenException();
					}
					if(trains.containsValue(overlap)){
						//comboio nas overlaps
						throw new CantSetGreenException();
					}
				}
			}
			reds.remove(t.sema);
		}else if(t instanceof PointOut){
			if(!ons.contains(t)){
				//PointOut nao esta ON
				throw new CantSetGreenException();
			}
			reds.remove(t.sema);
		}
	}
	
	public void toRed(Seg t) throws CantSetRedException{
		if (this.reds!= null && t != null && !this.reds.contains(t.sema)) this.setRed(t); 
		else throw new CantSetRedException();
	}
	
	//@ requires reds != null && t != null && t.n < t.nexts.length;
	public void toGreen(Seg t) throws CantSetGreenException{
		if (this.reds != null && t.sema != null && this.reds.contains(t.sema)) this.setGreen(t);
		else throw new CantSetGreenException();
	} 
	
	public void move(Train t,Seg s)  throws CantMoveException{
		try{
			if (this.trains != null && !this.trains.keySet().contains(t) && s!=null)	this.addTrain(t,s);
			
			else
			
			if (this.trains != null && this.trains.keySet().contains(t)) {
				
				Object track = this.trains.get((Object)t);
				
				if ((track instanceof PointIn)) {
					
					PointIn pi = (PointIn) track;
					if (agulha_off(pi)) {
						this.trains.remove(t);
						this.trains.put(t, pi.prox);
					} else throw new CantMoveException(new String("Agulha não está off!!!\n"));  
				} else {
					if ((track instanceof Track)) {
						Track trk = (Track) track;
						if (!(trk.sema != null && this.reds != null && this.reds.contains(trk.sema)) && 
								(!this.trains.containsValue(trk.next))) 
							this.moveTrain(t);
						else {throw new CantMoveException("Semáforo a vermelho! - Comboio em frente!");} 
					}
				}
			}
		}catch(Exception e){
			throw new CantMoveException("");
		}
		
	}

	private boolean agulha_off(PointIn seg){
		if (this.ons == null) return false;
		if (this.trains == null) return false;
		return ((!this.ons.contains(seg)) && (!this.trains.containsValue(seg)));
	}

	//@ requires pi!=null && po!=null && ons!=null && po.sema!=null && trains!=null && reds!=null;
	public void toOff(PointIn pi, PointOut po) throws CantSetOffException{
		if(this.ons!=null && pi!=null && po!=null && this.ons.contains(pi) && this.ons.contains(po)) setOff(pi,po);
		else { throw new CantSetOffException(); }
	}

	//@ requires pi!=null && po!=null && ons!=null && po.sema!=null && trains!=null && reds!=null;
	private void setOff(PointIn pi, PointOut po) throws CantSetOffException{
		//Se nao ha comboios nas agulhas e se o semaforo do POut esta a vermelho
		if(!trains.containsValue(po) && !trains.containsValue(pi) && this.reds.contains(po.sema)){
			//Se o PI tiver semaforo tambem esta a vermelho
			if(pi.sema==null || this.reds.contains(pi.sema)){
				ons.remove(pi);
				ons.remove(po);
			}else{
				throw new CantSetOffException();
			}
		}else{
			throw new CantSetOffException();
		}
	}

	//@ requires pi!=null && po!=null && ons!=null && po.sema!=null && trains!=null && reds!=null;
	public void toOn(PointIn pi, PointOut po) throws CantSetOnException{
		if(this.ons!=null && pi!=null && po!=null && !this.ons.contains(pi) && !this.ons.contains(po)) setOn(pi,po);
		else throw new CantSetOnException();
	}
	
	//@ requires pi!=null && po!=null && ons!=null && po.sema!=null && trains!=null && reds!=null;
	private void setOn(PointIn pi,PointOut po) throws CantSetOnException{
		if(!trains.containsValue(po) && !trains.containsValue(pi)) {
			ons.add(pi);
			ons.add(po);
		}else{
			throw new CantSetOnException();
		}
	}
	
	public static void main(){
        
        /*Track t1 = new Track();
        //Track t2 = new Track();
        //t1.setNext(t1);
        
        State estacao = new State(null,null,null);
        if (estacao != null)
        System.out.println("id1="+t1.getId()+"\nid2="+t2.getId());
        */
      
	        Semaphore sem = new Semaphore();
	        ArrayList array = new ArrayList();
	        
	        Track t2 = new Track();
	        Track t1 = new Track(t2,sem,array);
	        
	        Train t = new Train();
	        
	        HashMap train = new HashMap();
	        train.put(t,t1);
	        
	        ArrayList r = new ArrayList();
	        r.add(sem);
	        
	        State s = new State(train,r,null);                
	        
	        System.out.println(s.toString());
	        
	        try {
				s.toGreen(t1);
			} catch (CantSetGreenException e3) {
			
			}
	        
	        System.out.println(s.toString());
	        
	        try {
				s.move(t,t1);
			} catch (CantMoveException e) {
				System.out.println(e.toString());
			}
	        
	        System.out.println(s.toString());
	        
	        try {
				s.move(t,t1);
			} catch (Exception e) {
				System.out.println(e.toString());
			}
	        
	        System.out.println(s.toString());
	        
	        try {
				s.move(t, t1);
			} catch (Exception e) {
				System.out.println(e.toString());
			}
	        
	        System.out.println(s.toString());
	        
	        
	        
	
	}

	public String toString() {
	
	String s = new String();
	

	s += "---------------------------------------------\n";
	
	
	s += "Posicao dos Comnboios:\n";
	
	for (int i=0;trains != null && i < trains.size();i++)
	        s += i + " - " + trains.keySet().toArray()[i].toString() + " - em - " + (trains.values().toArray()[i] != null ? trains.values().toArray()[i].toString() : "fora") + "\n";
	
	s += "Semaforos a Vermelho:\n";
	
	for (int i=0;reds != null && i< reds.size();i++)
	        s += i + " - " + reds.toArray()[i].toString() + "\n";
	
	s += "Agulhas com Posicao a On:\n";
	
	for (int i=0;ons != null && i< ons.size();i++)
	        s += i + " - " + ons.toArray()[i].toString() + "\n";
	
	s += "---------------------------------------------\n";
	
	return s;
	}	
}
